A:MsgA, i:Id. Feasible(A)  (@i A) || (@i A) 

latex

Definitions	t  T, x:A. B(x), Id, s = t, Prop, ma-frame-compatible(A;B), M1 || M2, P & Q, P  Q, x:AB(x), P  Q, x:AB(x), P  Q, MsgA, Feasible(M), (@i M), A || B, ma-frame-compat(A;B)
Lemmas	ma-feasible wf, msga wf, m-at-compatible, Id wf, ma-compatible-self